% Equivalence Verifier
:- source.
:- use_module(library(lists)).

:- style_check(all).
:- yap_flag(unknown, error).

set_general_modules :-
	use_module('abc_parser.yap'),
	use_module('concrete.yap'),
	use_module('abstract.yap').

set_modules_for_expandable :-
	b_setval(policyname, 'noexpand'),

	use_module('hints/noexpand.yap'),
	use_module('abc_rewriter_expandable.yap').

set_modules_for_lookupswitch :-
	b_setval(policyname, 'lus'),

	use_module('hints/lookupswitch.yap'),
	use_module('hints_lookupswitch.yap'),
	use_module('abc_rewriter_lookupswitch.yap').

set_modules_for_resourcebound :-
	b_setval(policyname, 'rbound'),

	use_module('hints/navigate2.yap'),
	use_module('hints_resourcebound.yap'),
	use_module('abc_rewriter_resourcebounds.yap').

set_breakpoints :-
	spy(get_jump_target).


set_filenames(MFN, UFN, RFN, LFN, TFN) :-
	b_setval(markfile, MFN),
	b_setval(untrustedfile, UFN),
	b_setval(rewrittenfile, RFN),
	b_setval(logfile, LFN),
	b_setval(timefile, TFN).

%------------------------ TESTS -----------------

runatmosenergy :-
	set_general_modules,
	set_modules_for_resourcebound,
	set_filenames('Data/atmos-marked.txt', 'Data/atmos-untrusted.txt', 'Data/atmos-rewritten.txt', 'Data/atmos-log.txt', 'Data/atmos-time.txt'),
	check_equiv('URP/atmosenergy.abc','URP/Ratmosenergy.abc').

runatt :-
	set_general_modules,
	set_modules_for_resourcebound,
	set_filenames('Data/att-marked.txt', 'Data/att-untrusted.txt', 'Data/att-rewritten.txt', 'Data/att-log.txt', 'Data/att-time.txt'),
	check_equiv('URP/att.abc','URP/Ratt.abc').

%--------------------------------------------------

check_equiv(Untrusted,Rewritten) :- 
    
	% Use the appropriate hint module
	
	create_constraint_lists,
	
	b_getval(timefile, TimeFile),
	open(TimeFile, write, TStream),

	
	statistics(runtime, [PreRewriteTime, _]),
	rewrite(Untrusted,Rewritten, NewMarkedList, SecRelIndices),
	statistics(runtime, [PostRewriteTime, _]),
	RewriteTime is (PostRewriteTime-PreRewriteTime),
	write(TStream, 'Rewrite Time: '), write(TStream, RewriteTime), write(TStream, 'ms'), nl(TStream), 

	b_setval(secrelindices, SecRelIndices),
	b_setval(markedinstrlist, NewMarkedList),
	b_getval(markfile, MarkFile),
	open(MarkFile, write, MStream),
	print_marked_methods(NewMarkedList, MStream),
	close(MStream),

	get_AST(Untrusted, UntrustedAST),
	get_AST(Rewritten, RewrittenAST),

	b_setval(uast, UntrustedAST),
	b_setval(rast, RewrittenAST),

	% Print the Method Bodies to a File
	abc_parser:getABC(method_bodies, UntrustedAST, UMethods),
	abc_parser:getABC(method_bodies, RewrittenAST, RMethods),

	b_getval(untrustedfile, UntrustedFile),
	open(UntrustedFile, write, UStream),
	print_method_bodies(UMethods, UStream),
	close(UStream),
    
	b_getval(rewrittenfile, RewrittenFile),
	open(RewrittenFile, write, RStream),
	print_method_bodies(RMethods, RStream),
	close(RStream),
   
	b_getval(logfile, LogFile),
	open(LogFile, write, LogFile2),
	tell(LogFile2),

	statistics(runtime, [PreVerifTime, _]),
	init_abstract_interpret(run),
	statistics(runtime, [PostVerifTime, _]),
	VerifTime is (PostVerifTime-PreVerifTime),
	write(TStream, 'Verification Time: '), write(TStream, VerifTime), write(TStream, 'ms'), nl(TStream).

	
    
	
print_code([], _Stream).
print_code([I|Is], Stream) :-
	write(Stream, I),
	nl(Stream),
	print_code(Is, Stream).

print_method_bodies([], _Stream).
print_method_bodies([MB|MBs], Stream) :-
	print_method_body(MB, Stream),
	write(Stream, '\n'),
	print_method_bodies(MBs, Stream).
print_method_body(method_body(Method,_MS,_LC,_ISD,_MSD,_CL,C,_EC,_E,_TC,_T), Stream) :-
	write(Stream, 'Method is: '),
	write(Stream, Method),
	nl(Stream),
	print_code(C, Stream).

print_marked_methods([], Stream).
print_marked_methods([(MethNum-NMM) | NML], Stream) :-
	write(Stream, 'Method: '), write(Stream, MethNum),
	nl(Stream),
	print_code(NMM, Stream),
	nl(Stream),
	print_marked_methods(NML, Stream).
	
